﻿using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace O1.Kernel
{
    [ContractVerification(true)]
    internal class DurableCounter : SequenceProvider<int>
    {
        private int value;

        public DurableCounter(int value)
        {
            Contract.Requires(value > -1);

            this.value = value;
        }

        public override int Reserve(int rangeSize)
        {
            Contract.Assume(rangeSize > 0);

            var current = this.value;
            this.value += rangeSize;
            return current;
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(this.value > -1);
        }
    }
}
